/*
 * MinisatCover.cpp
 *
 *  Created on: 24 nov. 2011
 *  Authors: bnoleau, cybourdi, rlecrois
 */

#include "MinisatCover.h"

MinisatCover::MinisatCover() {
}

MinisatCover::~MinisatCover() {
}

bool MinisatCover::isSat(string s){
	return (strcmp(s.c_str(),"SAT") == 0);
}

list<int> MinisatCover::getMinisatCover(string fileName){
	ifstream minisatFile(fileName.c_str(), ios::in);
	list<int> numNodes;
	string isSatisfiable;

	if(minisatFile){
		minisatFile >> isSatisfiable;
		if(isSat(isSatisfiable)) {
			int numNode;
			minisatFile >> numNode;
			do {
				if (numNode > 0)
					numNodes.push_back(numNode);
				minisatFile >> numNode;
			} while(numNode != 0);
		}
		else
			cerr << "Le fichier Minisat possede un format incorrecte (la solution n'est pas satisfaisable)" << endl;
	}
	else
		cerr << "Impossible d'ouvrir le fichier !" << endl;

	return numNodes;
}

void lauchMinisatOnGraph(Graph* g) {
	MinisatBuilder b;
	g->build(&b);

	ofstream file("minisat-input", ios::out | ios::trunc);

	if (file) {
		file << b.getResult() << endl;
		file.close();
	} else
		cerr << "Erreur a l'ouverture !" << endl;

	system("minisat/core/minisat minisat-input minisat-output > /dev/null" );
}

list<int> MinisatCover::vertexCover(Graph* g) {

	lauchMinisatOnGraph(g);
	list<int> cover = getMinisatCover("minisat-output");
	return cover;
}
